;;;
;;; Solution for A3 question #4
;;;
;;; By Philip W. L. Fong
;;;

(defun resolution-initial-state (S)
  "Create initial state for refuting set S of clauses."
  (mapcar #'rename-variables S))

(defun resolution-successor-func (S)
  "Successor function for resolution refutation."
  (let ((top-clause (first S))
	(successor-list nil))
    (dolist (side-clause (rest S))
	    (dolist (resolvent (generate-resolvents top-clause side-clause))
		    (push (make-effect (list 'resolve top-clause 'with 
					     side-clause)
				       1
				       (cons (rename-variables resolvent) S))
			  successor-list)))
    successor-list))

(defun resolution-goal-test (S)
  "Goal test function for resolution refutation."
  (null (first S)))

(defun make-resolution-problem (S)
  "Create a search problem for refuting set S of clauses."
  (make-problem (resolution-initial-state S)
		#'resolution-successor-func 
		#'resolution-goal-test))

(defun refute (S strategy)
  "Refute set S of clauses by search strategy STRATEGY."
  (solve-problem (make-resolution-problem S) strategy))

